-
Notifications
You must be signed in to change notification settings - Fork 18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add checks for Enum #23
Conversation
ltordering a = succ a == Nothing || pred a < succ a | ||
|
||
predsuccpredLaw :: a -> Boolean | ||
predsuccpredLaw a = succ a == Nothing || (pred a >>= succ >>= pred) == pred a |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At first I thought this might be a typo and we should be checking pred a == Nothing
instead of succ a == Nothing
, but actually I think we can remove that check altogether:
If pred a
is Nothing
, then (pred a >>= succ >>= pred) == pred a
will always be true, regardless of whether you have a law-abiding Enum instance. If pred a
is Just something
, then whether (pred a >>= succ >>= pred) == pred a
holds depends on whether you have a law-abiding Enum instance.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right, the last two can get rid of the test.
gtordering a = succ a == Nothing || succ a > pred a | ||
|
||
ltordering ∷ a → Boolean | ||
ltordering a = succ a == Nothing || pred a < succ a |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is redundant; if gtordering
holds, and we have a law-abiding Ord
instance, then this will certainly hold. I think we should remove this law from the Enum class, really.
Sorry to be a bother but this has made me realise there are some issues with the |
Oops, didn't realise you were already discussing this over in |
@hdgarrood Can you suggest good names for the I also used crappy names there: https://github.com/garyb/purescript-quickcheck-laws/blob/master/src/Test/QuickCheck/Laws/Data/BoundedEnum.purs |
The
I'm not sure if that's necessarily an improvement, though. Also I'm not sure if 'homomorphism' is quite the right word here, because I've only really come across that word in group theory, where it refers to the interaction of a binary operation with a function like |
I'm doubting now the enumpred/enumsucc laws make sense. Isn't it possible to have, say, an enum mapping only to even values? |
Hmm, I don't think so, that's what the laws are there to prevent. You could have an |
I found this: https://hackage.haskell.org/package/proto-lens-0.1.0.2/src/src/Data/ProtoLens/Message/Enum.hs Shouldn't those be relaxed to:
|
Let's say you wanted to wrap libavcodec: If we want to represent that with an enum I think we should relax the rules. |
We don't - or at least, not like that. The way to do it would be to create an ADT for that enum, and then convert it back into a numeric value when using it with the FFI. |
Yeah, I agree with @garyb, that's not what an enumeration is in my mind. In my mind an enumeration of a set X is a bijection from the natural numbers to X (or perhaps, instead of the whole set of natural numbers, you might have a finite subset of the natural numbers of the form {1,2,3,...n} for some fixed number n). In that sense, You can certainly create an ADT for codecs like that, and so of course you'll need functions to attempt conversions to and from the numeric representation that libavcodec uses, but I don't think these functions should live inside the |
Actually looking at the source, I think we should probably have
but the code seems to assume that we will have |
Oh, wait, the |
Yeah, I don't think |
It's true that trying to model C enums via PS enums might not be a good idea, given that several names in a C enum can refer to the same value. But I also want to understand what does having contiguous values bring to the table. |
I think, for me, it's mainly that that is what the word 'enumeration' implies, i.e. that it means the name is appropriate. Also, I don't think requiring contiguousness will rule out many useful instances either. If you can define an I guess it also means you can do things like, if you know you want to find the nth successor of something, you can do |
Should this PR be closed? |
Possibly, but it would be helpful if you could include some reasoning as to why you think we might want to consider closing this. Are we deciding we don't want to implement checks for Enum in this library at all, or is there a problem with this implementation in particular, or what? |
I was proposing we close this mainly due to inactivity. I think checks for |
I think we should only close PRs for inactivity if the original submitter is not responsive to questions. That isn't what has happened here - a number of commits have been pushed since the last review. I personally think that we should leave it open until we either:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code here looks good to me. I think the EuclideanRing test changes are due to #30, which should be fixed in #58.
But that being said, aren't there cases where an enumeration could lead to integer overflow if one's starting int is very high? Should the docs be updated to mention the possibility of integer overflow?
Current CI failures: no
|
CI now builds. |
Can this PR get another review? |
Again, names are intentionally ugly to ensure someone suggests better ones ;)